Natural Deduction in MLTT

Inductive ND_proves : list (prop atom) -> prop atom -> Prop :=
| ND_exfalso_quodlibet {Γ P} : Γ ⊢ ⊥ -> Γ ⊢ P
| ND_True_intro {Γ} : Γ ⊢ ⊤
| ND_or_introl {Γ P Q} : Γ ⊢ P -> Γ ⊢ P ∨ Q
| ND_or_intror {Γ P Q} : Γ ⊢ Q -> Γ ⊢ P ∨ Q
| ND_proof_by_cases {Γ P Q R} : Γ ⊢ P ∨ Q -> P :: Γ ⊢ R -> Q :: Γ ⊢ R -> Γ ⊢ R
| ND_and_intro {Γ P Q} : Γ ⊢ P -> Γ ⊢ Q -> Γ ⊢ P ∧ Q
| ND_and_elim {Γ P Q R} : Γ ⊢ P ∧ Q -> P :: Q :: Γ ⊢ R -> Γ ⊢ R
| ND_cond_proof {Γ P Q} : P :: Γ ⊢ Q -> Γ ⊢ P ⊃ Q
| ND_modus_ponens {Γ P Q} : Γ ⊢ P ⊃ Q -> Γ ⊢ P -> Γ ⊢ Q
| ND_assumption {Γ P} : In P Γ -> Γ ⊢ P
| ND_cut {Γ P Q} : Γ ⊢ P -> P :: Γ ⊢ Q -> Γ ⊢ Q
where "Γ ⊢ P" := (ND_proves Γ P).